package mechanism.dbc;

import java.util.Arrays;

import junit.framework.TestCase;

/* 
 * 该队列的契约性定义：
 * 
 * 1．先验条件（应用于put（））：不允许将空元素添加到队列中。
 * 2．先验条件（应用于put（））：向满队列添加元素是非法的。
 * 3．后验条件（应用于get（））：从空队列取元素是非法的。
 * 4．后验条件（应用于get（））：不能从数组中产生空元素。
 * 5．不变量：数组中包含对象的区域不能有任何空元素。
 * 6．不变量：数组中不包含对象的区域必须仅有空值。
 */

public class MyQueue {

	// Design-by-contract support methods:
	private static void precondition(boolean cond, String msg) {
		if (!cond)
			throw new QueueException(msg);
	}

	// Design-by-contract support methods:
	private static boolean postcondition(boolean cond, String msg) {
		if (!cond)
			throw new QueueException(msg);
		return true;
	}

	private Object[] data;

	// Next available storage space
	private int in = 0;

	// Next gettable object
	private int out = 0;

	// Has it wrapped around the circular queue?
	private boolean wrapped = false;

	public MyQueue(int size) {
		data = new Object[size];
		assert invariant(); // Must be true after construction
	}

	public boolean empty() {
		return !wrapped && in == out;
	}

	public boolean full() {
		return wrapped && in == out;
	}

	public void put(Object item) {
		precondition(item != null, "put() null item");
		precondition(!full(), "put() into full Queue");
		assert invariant();
		data[in++] = item;
		if (in >= data.length) {
			in = 0;
			wrapped = true;
		}
		assert invariant();
	}

	public Object get() {
		precondition(!empty(), "get() from empty Queue");
		assert invariant();
		Object returnVal = data[out];
		data[out] = null;
		out++;
		if (out >= data.length) {
			out = 0;
			wrapped = false;
		}
		assert postcondition(returnVal != null, "Null item in Queue");
		assert invariant();
		return returnVal;
	}

	private boolean invariant() {
		// Guarantee that no null values are in the
		// region of 'data' that holds objects:
		for (int i = out; i != in; i = (i + 1) % data.length)
			if (data[i] == null)
				throw new QueueException("null in queue");
		// Guarantee that only null values are outside the
		// region of 'data' that holds objects:
		if (full())
			return true;
		for (int i = in; i != out; i = (i + 1) % data.length)
			if (data[i] != null)
				throw new QueueException("non-null outside of queue range: "
						+ dump());
		return true;
	}

	private String dump() {
		return "in = " + in + ", out = " + out + ", full() = " + full()
				+ ", empty() = " + empty() + ", queue = " + Arrays.asList(data);
	}

	public static class QueueException extends RuntimeException {
		public QueueException(String why) {
			super(why);
		}
	}

	// JUnit testing.
	// As an inner class, this has access to privates:
	public static class WhiteBoxTest extends TestCase {
		private MyQueue queue = new MyQueue(10);
		private int i = 0;

		public WhiteBoxTest(String name) {
			super(name);
			while (i < 5)
				// Preload with some data
				queue.put("" + i++);
		}

		// Support methods:
		private void showFullness() {
			assertTrue(queue.full());
			assertFalse(queue.empty());
			// Dump is private, white-box testing allows access:
			System.out.println(queue.dump());
		}

		private void showEmptiness() {
			assertFalse(queue.full());
			assertTrue(queue.empty());
			System.out.println(queue.dump());
		}

		public void testFull() {
			System.out.println("testFull");
			System.out.println(queue.dump());
			System.out.println(queue.get());
			System.out.println(queue.get());
			while (!queue.full())
				queue.put("" + i++);
			String msg = "";
			try {
				queue.put("");
			} catch (QueueException e) {
				msg = e.getMessage();
				System.out.println(msg);
			}
			assertEquals(msg, "put() into full Queue");
			showFullness();
		}

		public void testEmpty() {
			System.out.println("testEmpty");
			while (!queue.empty())
				System.out.println(queue.get());
			String msg = "";
			try {
				queue.get();
			} catch (QueueException e) {
				msg = e.getMessage();
				System.out.println(msg);
			}
			assertEquals(msg, "get() from empty Queue");
			showEmptiness();
		}

		public void testNullPut() {
			System.out.println("testNullPut");
			String msg = "";
			try {
				queue.put(null);
			} catch (QueueException e) {
				msg = e.getMessage();
				System.out.println(msg);
			}
			assertEquals(msg, "put() null item");
		}

		public void testCircularity() {
			System.out.println("testCircularity");
			while (!queue.full())
				queue.put("" + i++);
			showFullness();
			// White-box testing accesses private field:
			assertTrue(queue.wrapped);
			while (!queue.empty())
				System.out.println(queue.get());
			showEmptiness();
			while (!queue.full())
				queue.put("" + i++);
			showFullness();
			while (!queue.empty())
				System.out.println(queue.get());
			showEmptiness();
		}
	}
}
